algebraic fundamentally means equational
| title | "algebraic" fundamentally means "equational" |
|---|
-
: it's all about stating that certain expressions are equal to other expressions
-
structures like groups, rings, and fields are defined entirely through equations, like associativity, commutativity, distributivity, etc
-
GAT extends algebraic theories but maintain the same fundamental restriction: they can only express equational axioms.
-
Non-example: what GAT cannot express
- existential statements: there exists x such that ...
- inequalities: x < y, x != y
- logical implications that aren't reducible to equations
- higher-order logic